\begin{tabbing}
usends1{-}p(${\it es}$;${\it ds}$;$k$;$T$;$l$;${\it tg}$;$B$;$f$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=(($\forall$$x$:Id. subtype\_rel(es{-}vartype(${\it es}$; source($l$); $x$); fpf{-}cap(${\it ds}$; id{-}deq; $x$; top)))\+
\\[0ex]$\wedge$ alle{-}at(\=${\it es}$;\+
\\[0ex]source($l$);
\\[0ex]$e$.((es{-}kind(${\it es}$; $e$) = $k$) $\Rightarrow$ subtype\_rel(es{-}valtype(${\it es}$; $e$); $T$)))
\-\\[0ex]$\wedge$ ($\forall$$e$:es{-}E(${\it es}$). (es{-}kind(${\it es}$; $e$) = rcv($l$,${\it tg}$)) $\Rightarrow$ subtype\_rel(es{-}valtype(${\it es}$; $e$); $B$)))
\\[0ex]c$\wedge$ alle{-}at(\=${\it es}$;\+
\\[0ex]source($l$);
\\[0ex]$e$.((es{-}kind(${\it es}$; $e$) = $k$)
\\[0ex]$\Rightarrow$ ($\exists$\=${\it e'}$:es{-}E(${\it es}$)\+
\\[0ex]((es{-}kind(${\it es}$; ${\it e'}$) = rcv($l$,${\it tg}$))
\\[0ex]c$\wedge$ \=((es{-}sender(${\it es}$; ${\it e'}$) = $e$)\+
\\[0ex]$\wedge$ \=($\forall$${\it e''}$:es{-}E(${\it es}$). \+
\\[0ex](es{-}kind(${\it es}$; ${\it e''}$) = rcv($l$,${\it tg}$))
\\[0ex]$\Rightarrow$ (es{-}sender(${\it es}$; ${\it e''}$) = $e$)
\\[0ex]$\Rightarrow$ (${\it e''}$ = ${\it e'}$))
\-\\[0ex]$\wedge$ (es{-}val(${\it es}$; ${\it e'}$) = $f$(es{-}state{-}when(${\it es}$; $e$),es{-}val(${\it es}$; $e$))))))))
\-\-\-\-
\end{tabbing}